/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRK30



␈↓ ↓H␈↓␈↓ βJ␈↓¬ON THE MODEL THEORY OF KNOWLEDGE␈↓



␈↓ ↓H␈↓The␈αneed␈α
to␈αrepresent␈α
information␈αabout␈α
who␈αknows␈α
what␈αin␈α
intelligent␈αcomputer␈α
programs␈αwas
␈↓ ↓H␈↓the␈α
original␈α
motivation␈α
for␈αthis␈α
work.␈α
 For␈α
example,␈α
a␈αprogram␈α
that␈α
arranges␈α
trips␈α
must␈αknow␈α
that
␈↓ ↓H␈↓travel␈α
agents␈α
know␈α∞who␈α
knows␈α
the␈α
availability␈α∞of␈α
rooms␈α
in␈α
hotels.␈α∞ An␈α
early␈α
problem␈α
is␈α∞how␈α
to
␈↓ ↓H␈↓represent␈αwhat␈α
people␈αknow␈αabout␈α
other␈αpeople's␈αknowledge␈α
of␈αfacts,␈αand␈α
even␈αthe␈α
knowledge␈αof
␈↓ ↓H␈↓propositions␈α⊂treated␈α⊂in␈α⊂this␈α⊂paper␈α⊂presented␈α⊃some␈α⊂problems␈α⊂that␈α⊂were␈α⊂not␈α⊂treated␈α⊃in␈α⊂previous
␈↓ ↓H␈↓literature.

␈↓ ↓H␈↓We␈αstarted␈αwith␈αthe␈αfollowing␈αwell␈αknown␈αpuzzle␈αof␈αthe␈αthree␈αwise␈αmen:␈α␈↓↓␈αA␈αking␈αwishing␈αto␈αknow
␈↓ ↓H␈↓↓which␈αof␈α
his␈αthree␈α
wise␈αmen␈αis␈α
the␈αwisest,␈α
paints␈αa␈α
white␈αspot␈αon␈α
each␈αof␈α
their␈αforeheads,␈αtells␈α
them
␈↓ ↓H␈↓↓at␈α∂least␈α∂one␈α∂spot␈α∂is␈α∂white,␈α∂and␈α∂asks␈α∂each␈α∞to␈α∂determine␈α∂the␈α∂color␈α∂of␈α∂his␈α∂spot.␈α∂ After␈α∂a␈α∂while␈α∞the
␈↓ ↓H␈↓↓smartest␈αannounces␈αthat␈αhis␈αspot␈αis␈αwhite␈αreasoning␈αas␈αfollows:␈α "Suppose␈αmy␈αspot␈αwere␈αblack.␈α The
␈↓ ↓H␈↓↓second␈α
wisest␈α
of␈α
us␈α
would␈α
then␈α
see␈α
a␈α
black␈α
and␈α
a␈α
white␈α
and␈α
would␈α
reason␈α
that␈α
if␈α
his␈α
spot␈α
were␈α
black,
␈↓ ↓H␈↓↓the␈αdumbest␈αwould␈αsee␈αtwo␈αblack␈αspots␈αand␈αwould␈αconclude␈αthat␈αhis␈αspot␈αis␈αwhite␈αon␈αthe␈αbasis␈αof␈αthe
␈↓ ↓H␈↓↓king's assurance.  He would have announced it by now, so my spot must be white."␈↓

␈↓ ↓H␈↓In␈αformalizing␈α
the␈αpuzzle,␈αwe␈α
don't␈αwish␈αto␈α
try␈αto␈α
formalize␈αreasoning␈αabout␈α
how␈αfast␈αother␈α
people
␈↓ ↓H␈↓reason.␈α
 Therefore,␈α
we␈α
will␈α
imagine␈α
that␈α
either␈α∞the␈α
king␈α
asks␈α
the␈α
wise␈α
men␈α
in␈α∞sequence␈α
whether
␈↓ ↓H␈↓they␈αknow␈αthe␈αcolors␈αof␈αtheir␈α
spots␈αor␈αthat␈αhe␈αasks␈αsynchronously,␈α
"Do␈αyou␈αknow␈αthe␈αcolor␈αof␈α
your
␈↓ ↓H␈↓spot"␈α
getting␈α
a␈α
chorus␈α
of␈α
noes.␈α He␈α
asks␈α
it␈α
again␈α
with␈α
the␈αsame␈α
result,␈α
but␈α
on␈α
the␈α
third␈αasking,␈α
they
␈↓ ↓H␈↓answer␈α∂that␈α∂their␈α⊂spots␈α∂are␈α∂white.␈α∂ Needless␈α⊂to␈α∂say,␈α∂we␈α∂are␈α⊂also␈α∂not␈α∂formalizing␈α∂any␈α⊂notion␈α∂of
␈↓ ↓H␈↓relative wisdom.

␈↓ ↓H␈↓We␈αstart␈αwith␈αa␈α
general␈αset␈αof␈αaxioms␈α
for␈αknowledge␈αbased␈αon␈α
the␈αnotation,␈αaxioms,␈αand␈α
inference
␈↓ ↓H␈↓rules␈α
of␈α
propositional␈α
calculus␈α
supplemented␈α
by␈α
the␈α
notation␈α
␈↓↓S*p␈↓␈α
standing␈α
for,␈α
"Person␈α
S␈αknows
␈↓ ↓H␈↓proposition␈α⊃p."␈α⊃ Thus␈α⊃␈↓↓W3*W2␈↓πj␈↓↓(W1*p1)␈↓␈α⊃can␈α⊃stand␈α⊃for,␈α⊃"The␈α⊃third␈α⊃wise␈α⊃man␈α⊃knows␈α⊃that␈α⊂the
␈↓ ↓H␈↓second␈α∞wise␈α
man␈α∞knows␈α
that␈α∞the␈α
first␈α∞wise␈α∞man␈α
does␈α∞not␈α
know␈α∞that␈α
the␈α∞first␈α
wise␈α∞man's␈α∞spot␈α
is
␈↓ ↓H␈↓white".

␈↓ ↓H␈↓We␈α⊃use␈α⊃axiom␈α⊃achemata␈α⊃with␈α⊃subscripted␈α⊃S's␈α⊂as␈α⊃person␈α⊃variables,␈α⊃subscripted␈α⊃p's␈α⊃and␈α⊃q's␈α⊂as
␈↓ ↓H␈↓propositional␈α∞variables,␈α∞and␈α∞a␈α∞special␈α
person␈α∞constant␈α∞called␈α∞"any␈α∞fool"␈α
and␈α∞denoted␈α∞by␈α∞0.␈α∞ It␈α
is
␈↓ ↓H␈↓convenient␈α∂to␈α∂introduce␈α∂"any␈α∂fool"␈α∂because␈α∞whatever␈α∂he␈α∂knows,␈α∂every␈α∂one␈α∂knows␈α∂everyone␈α∞else
␈↓ ↓H␈↓knows.␈α "Any␈α
fool"␈αis␈α
especially␈αuseful␈αwhen␈α
an␈αevent␈α
occurs␈αin␈αfront␈α
of␈αall␈α
the␈αknowers,␈α
and␈αwe
␈↓ ↓H␈↓need a sentence like, "S1 knows that S2 knows that S3 knows etc.".  Here are the schemata:

␈↓ ↓H␈↓K0:␈↓ αλS*p ⊃ p; What a person knows is true.

␈↓ ↓H␈↓K1:␈↓ αλ0*(S*p ⊃ p); Any fool knows that what a person knows is true.

␈↓ ↓H␈↓K2:␈↓ αλ0*(0*p␈α
⊃␈α0*S*p);␈α
What␈α
any␈αfool␈α
knows,␈αany␈α
fool␈α
knows␈αeveryone␈α
knows,␈αand␈α
and␈α
any␈αfool
␈↓ ↓H␈↓␈↓ α_knows that.

␈↓ ↓H␈↓K3:␈↓ αλ0*(S*p ∧ S*(p ⊃ q) ⊃ S*q); Any fool knows everyone can do modus ponens.

␈↓ ↓H␈↓There are two optional schemata K4 and K5:
␈↓ ↓H␈↓␈↓ εH␈↓ 91


␈↓ ↓H␈↓K4:␈↓ αλ0*(S*p ⊃ S*S*p); Any fool knows that what someone knows, he knows he knows.

␈↓ ↓H␈↓K5:␈↓ αλ0*(␈↓πj␈↓S*p␈α
⊃␈α∞S*␈↓πj␈↓S*p);␈α
Any␈α∞fool␈α
knows␈α∞that␈α
what␈α
someone␈α∞doesn't␈α
know␈α∞he␈α
knows␈α∞he␈α
doesn't
␈↓ ↓H␈↓␈↓ α_know.

␈↓ ↓H␈↓If␈αthere␈αis␈αonly␈α
one␈αperson␈αS,␈αthe␈αsystem␈α
is␈αequivalent␈αto␈αa␈α
system␈αof␈αmodal␈αlogic.␈α Axioms␈α
K0-K3
␈↓ ↓H␈↓give␈αa␈αsystem␈α
equivalent␈αto␈αwhat␈α
Hughes␈αand␈αCresswell[1]␈αcall␈α
T,␈αand␈αK4␈α
and␈αK5␈αgive␈αthe␈α
modal
␈↓ ↓H␈↓systems␈αS4␈αand␈αS5␈αrespectively.␈α We␈αcall␈αK4␈αand␈αK5␈αthe␈αintrospective␈αschemata.␈α It␈αis␈αconvenient
␈↓ ↓H␈↓to write S␈↓∧1␈↓p as an abbreviation for S*p ∨ S* ␈↓πj␈↓ p; it may be read, "S knows whether p".

␈↓ ↓H␈↓On the basis of these schemata we may axiomatize the wise man problem as follows:
␈↓ ↓H␈↓C0:  p1 ∧ p2 ∧ p3
␈↓ ↓H␈↓C1:  0*(p1 ∨ p2 ∨ p3)
␈↓ ↓H␈↓C2:  0*(S1$p2 ∧ S1$p3 ∧ S2$p1 ∧ S2$p3 ∧ S3$p1 ∧ S3$p2)
␈↓ ↓H␈↓C3:  0*(S2$S1-p1)
␈↓ ↓H␈↓C4:  0*(S3$S2*p2)
␈↓ ↓H␈↓C5:  ␈↓πj␈↓S1$p1
␈↓ ↓H␈↓C6:  ␈↓πj␈↓S2$p2

␈↓ ↓H␈↓From␈α
K0-K3␈α
and␈α
C1-C6␈α
it␈α
is␈α
possible␈α
to␈α
prove␈αS3*p3.␈α
 C0␈α
is␈α
not␈α
used␈α
in␈α
the␈α
proof.␈α
In␈αsome␈α
sense
␈↓ ↓H␈↓C5␈αand␈αC6␈αshould␈αnot␈αbe␈αrequired.␈α Looking␈αat␈αthe␈αproblem␈αsequentially,␈αit␈αshould␈αfollow␈αthat␈α
S1
␈↓ ↓H␈↓does not know p1 initially, an that even knowing that, S2 doesn't know p2.

␈↓ ↓H␈↓In␈α∪order␈α∪to␈α∩proceed␈α∪further␈α∪with␈α∩the␈α∪problem,␈α∪model␈α∩theoretic␈α∪semantics␈α∪is␈α∪necessary.␈α∩ The
␈↓ ↓H␈↓semantics␈α∀we␈α∀give␈α∀is␈α∀a␈α∪generalization␈α∀of␈α∀that␈α∀for␈α∀modal␈α∪logics␈α∀due␈α∀to␈α∀Kripke.␈α∀ Using␈α∪the
␈↓ ↓H␈↓completeness␈α∂result␈α∞of␈α∂our␈α∂systems␈α∞for␈α∂Kripke-type␈α∞semantics,␈α∂we␈α∂have␈α∞given␈α∂a␈α∂model␈α∞theoretic
␈↓ ↓H␈↓solution of the puzzle.

␈↓ ↓H␈↓We␈α
also␈α∞deal␈α
with␈α∞formal␈α
analysis␈α∞of␈α
the␈α∞puzzle␈α
of␈α∞unfaithful␈α
wives␈α∞along␈α
the␈α∞same␈α
line,␈α∞but␈α
it
␈↓ ↓H␈↓requires to treat the notion of time as well.  The reader is referred to Sato[2] for details.

␈↓ ↓H␈↓␈↓ ¬y␈↓¬References␈↓


␈↓ ↓H␈↓[1]␈↓ αλHughes,␈αG.E.,␈αand␈αCresswell,␈αM.J.,␈α␈↓αAn␈αIntroduction␈αto␈αModal␈αLogic␈↓,␈αLondon:␈αMethuen␈αand
␈↓ ↓H␈↓␈↓ α_Co., 1968.

␈↓ ↓H␈↓[2]␈↓ αλSato,␈αM.,␈α
␈↓↓A␈αstudy␈α
of␈αKripke-type␈α
models␈αfor␈α
some␈αmodal␈α
logics␈αby␈α
Gentzen's␈αsequential␈α
method␈↓,
␈↓ ↓H␈↓␈↓ α_Technical␈αReport␈αRIMS-206,␈αRIMS,␈αKyoto␈αUniversity␈α1976,␈αto␈αappear␈αin␈αPubl.␈αRIMS,␈α
Vol.
␈↓ ↓H␈↓␈↓ α_13, No. 2, 1977.